int_1_intro 9,38
Definitions of inequality predicates on integers and
common integer subtypes. 

Also includes induction lemmas for naturals, and
experiment proving theorem with Ycombinator extract. 

origin